ds:x:Id fp Type, da:k:Knd fp Type, es:ES, i:Id, e1, e2:{e:E| loc(e) = i }, e:E.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 (e1 <loc e)
 e  e2 
 es-hist{i:l}(es;e1;e2)
 =
 (es-hist{i:l}(es;e1;pred(e)) @ es-hist{i:l}(es;e;e2))
  event-info(ds;da) List 

latex

Definitions	t  T, P & Q, P  Q, x:A. B(x), P  Q, pred(e), 1of(t), E, [e, e'], Top, es-hist{i:l}(es;e1;e2), Id, x. t(x), a:A fp B(a), Knd, ES, loc(e), IdDeq, f(x)?z, vartype(i;x), kind(e), KindDeq, valtype(e), (e <loc e'), e  e' , event-info(ds;da), b, False, A, as @ bs, S  T, Prop, {T}, SQType(T), (x  l), es-info(es;e), map(f;as)
Lemmas	es-info wf, map wf, event-info wf, member-es-interval, subtype rel list, l member wf, list-subtype, Id sq, es-interval wf2, es-interval-partition, es-le-loc, es-loc-pred, es-le wf, es-locl wf, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-loc wf, event system wf, Knd wf, fpf wf, Id wf, map append sq, es-E wf, es-interval wf, es-pred wf, es-locl-iff